Inference at * 2 1 2 
Iof proof for Lemma p-fun-exp-compose:



1. T : Type
2. n : 
3. 0 < n
4. h, f:(T(T + Top)). f^n - 1 o h   = primrec(n - 1;h;i,g. f o g  )
5. h : T(T + Top)
6. f : T(T + Top)
  f o primrec(n - 1;p-id();i,g. f o g  )   o h   = f o primrec(n - 1;h;i,g. f o g  )   

latex

 by (Fold `p-fun-exp` 0) 
CollapseTHEN ((RWO "p-compose-associative<" 0) 
CollapseTHEN ((Auto) 

CoCollapseTHEN ((EqCD) 
CollapseTHEN ((Auto) 
CollapseTHEN ((if ((0
C) = 0) then BackThruSomeHyp else BHyp (0) )))))) 

latex

C.

Definitions	P  Q, P & Q, x:A  B(x), f^n, P  Q, P  Q, f o g  , Type, T, s = t, x:AB(x), left + right, Top, x:A. B(x), True, t  T
Lemmas	p-compose-associative, p-compose wf, squash wf, true wf, top wf